﻿module CoreEx
(* module CoreEx is used for extending the Core language AST with a context-graph "attached" to each node.
   It is used in the abstract-interpreter algorithm to hold the partial / temporary and eventually final interpretation
   result graphs of each of the AST nodes analysis. *)

(* datatype used for defining the AST extended with context-graph "attached" to each node. *)
type CmdEx = Skip | Asgn of int * Core.Expr | Choice of Cmd * Cmd | Seq  of Cmd * Cmd  | Loop of int * Cmd | Goto of string | Label of string

and Cmd = AICmd of CmdEx * (ContextGraph.graph ref) * int (* Constructor for a command with a graph "attached" and an identifier. *)

(* this function raises an exception if the given AST contains an assignment command
    of the form Xi := e inside a loop whose counter variable is Xi, s.t. e <> Xi. *)
let rec verifyLoopVarsUnmodifiedInsideLoopBodies(c : Core.Cmd) =
    let raiseLoopVarModifiedException(i) =
        failwith ("Loop variable '" + Parser.parserLastVarToIndexMap().[i].ToString() + "' modified inside loop body.")

    let rec verifyVarUnmodifiedByCmd(i : int, c' : Core.Cmd) =
        match c' with
        | Core.Asgn(i',e) ->
            if i = i' then
                match e with
                | Core.Var x ->
                    if x <> i then raiseLoopVarModifiedException(i)
                    else ()
                | _ -> raiseLoopVarModifiedException(i)
            else ()
        | Core.Choice(c1,c2)  -> (verifyVarUnmodifiedByCmd(i,c1);verifyVarUnmodifiedByCmd(i,c2))
        | Core.Seq(c1,c2)     -> (verifyVarUnmodifiedByCmd(i,c1);verifyVarUnmodifiedByCmd(i,c2))
        | Core.Loop(i',c)     -> (verifyVarUnmodifiedByCmd(i,c);verifyVarUnmodifiedByCmd(i',c))
        | _ -> ()

    match c with
        | Core.Loop(i,c)     -> verifyVarUnmodifiedByCmd(i,c)
        | Core.Seq(c1,c2)    -> (verifyLoopVarsUnmodifiedInsideLoopBodies(c1);
                                    verifyLoopVarsUnmodifiedInsideLoopBodies(c2))
        | Core.Choice(c1,c2) -> (verifyLoopVarsUnmodifiedInsideLoopBodies(c1);
                                    verifyLoopVarsUnmodifiedInsideLoopBodies(c2))
        | _ -> ()

(* converts a regular AST to an extended AST ready for the Abstract Interpreter algorithm.
    Note:  loop body command c is expanded to: "if { c } else { Skip }".
    This is done to avoid calculating the Skip graph explicitly by the abstact interpreter algorithm. *)
let rec extendedAbsIntAST(c) =
    let j = ref 0
    let rec extAST = function
        | (Core.Skip)          -> AICmd(Skip, ref (ContextGraph.newGraph([])),!j)
        | (Core.Goto(lbl))     -> AICmd(Goto(lbl), ref (ContextGraph.newGraph([])),!j)
        | (Core.Label(lbl))    -> AICmd(Label(lbl), ref (ContextGraph.newGraph([])),!j)
        | (Core.Asgn(i,e))     -> AICmd(Asgn(i,e), ref (ContextGraph.newGraph([])),!j)
        | (Core.Choice(c1,c2)) -> AICmd(Choice(extAST'(c1), extAST'(c2)), ref (ContextGraph.newGraph([])),!j)
        | (Core.Seq(c1,c2))    -> AICmd(Seq(extAST'(c1), extAST'(c2)), ref (ContextGraph.newGraph([])),!j)
        | (Core.Loop(i,c))     -> AICmd(Loop(i, extAST'(Core.Choice(Core.Skip,c))), ref (ContextGraph.newGraph([])),!j);
    and extAST'(c) =
        let cExt = extAST(c)
        let () = j := !j + 1
        cExt
    let () = verifyLoopVarsUnmodifiedInsideLoopBodies(c)
    extAST'(c)

(* converts an extended AST to a regular AST. This letction is not the inverse of the extendedAST letction (due to the loop expansion). *)
let rec reducedAST = function
    | (AICmd(Skip, _,_))         -> Core.Skip
    | (AICmd(Goto(lbl), _,_))    -> Core.Goto(lbl)
    | (AICmd(Label(lbl), _,_))    -> Core.Label(lbl)
    | (AICmd(Asgn(i,e),_,_))     -> Core.Asgn(i,e)
    | (AICmd(Choice(c1,c2),_,_)) -> Core.Choice(reducedAST(c1),reducedAST(c2))
    | (AICmd(Seq(c1,c2),_,_))    -> Core.Seq(reducedAST(c1),reducedAST(c2))
    | (AICmd(Loop(i,c),_,_))     -> Core.Loop(i,reducedAST(c))

(* extracts the graph of a CoreEx.Cmd *)
let graph = function
    | (AICmd(_,g,_)) -> g

let pat = function
    | AICmd(Skip,_,_) -> Pattern.Skip
    | AICmd(_,_,id)  -> Pattern.Cmd(id)

let id = function
         | (AICmd(_,_,id')) -> id'

(* prints the reduced AST of c *)
let prt(c) = Core.prt(reducedAST(c));